We extend standard session-typed languages (see, e.g.,~\cite{DBLP:conf/esop/HondaVK98,DBLP:journals/entcs/YoshidaV07})
with \emph{located processes} and \emph{update actions}.
These two constructs, extracted from~\cite{BGPZFMOODS}, allow us to explicitly represent runtime adaptation 
within models of structured communications.
This section introduces the syntax and semantics of our process model, 
and illustrates some of the adaptation patterns expressible in it.\done\todo[B27.]{Fixed, dropping "we introduce", pls check.}
%\jp{As I explain below, we could (and probably should) avoid saying the following sentence.}
%As in~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
%our process language 
%is instrumented with some elements which support the static analysis.
%In particular, we  
%annotate 
%located processes with an integer (representing established sessions).

\subsection{Syntax}
Our syntax builds upon the following  (disjoint)
base sets: 
\emph{names}, ranged over $a, b,  \ldots$;
\emph{locations}, ranged over $l, l', \ldots$;
\emph{labels}, ranged over $n, n', \ldots$;
\emph{constants} (integers, booleans, names), ranged over $c, c', \ldots$;\done\todo[C7.]{We have dropped "arithmetic" and have added other operations for constants.}
\emph{process variables}, ranged over $\mathsf{X}, \mathsf{X}', \ldots$.
%The sets of names and locations are assumed disjoint.
Then, \emph{processes}, ranged over $P, Q, R, \ldots$
and \emph{expressions}, ranged over $e, e', \ldots$
are given by the grammar in Table \ref{tab:syntax}.
%Our semantics uses 
We write $\widetilde{e}$ to denote 
a finite sequence of expressions $e_1, \ldots, e_n$; a similar convention applies for variables.
Notice that we also use 
\emph{(polarized) channels}, ranged over $\cha^{p}, \cha_1^{p}, \ldots$, where $p \in \{+,-\}$.
%and \emph{integers}, ranged over $j,h,m,\ldots$.
%Notice that we use identifier $k$ to denote  channels $\cha^{p}$ and names $x$.
\done\todo[B3.]{Here I have removed the reference to the semantics. We have clarified the channel/names notation in Table~\ref{tab:syntax}.}
In the following,  $j,h,m,\ldots$  range over 
%\emph{integers}.
$\mathbb{N}$.%\footnote{J: Cinzia, check this.}


%\emph{recursion variables}, ranged over $Y, Y', \ldots$;



\begin{table}[t]
$$
\begin{array}{lrlr}
a, b, c & ::=  &   x, y, z  & \text{variables}	\\
& \sepr &  u, v, w  & \text{names}	\\
 k & ::=  &   x, y, z  & \text{variables}	\\
& \sepr& \cha^{+}, \cha^{-} & \text{channels}	\\
P & ::=  &   \nopenr{a}{x}.P  & \text{session request}	\\
	& \sepr &   \nopena{a}{x}.P  & \text{session acceptance}	\\
	       & \sepr & \repopen{a}{x}.P  & \text{persistent session acceptance}	\\
	& \sepr &  \outC{k}{\widetilde{e}}.P & \text{data output}\\
  	&\sepr &    \inC{k}{\widetilde{x}}.P  & \text{data input}\\
	& \sepr &  \throw{k}{k'}.P & \text{channel output}\\
    &\sepr &   \catch{k}{x}.P  & \text{channel input}\\
	&\sepr&   \select{k}{n};P & \text{selection}\\
    	&\sepr&   \branch{k}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m} & \text{branching}\\
%	&\sepr&  \component{l}{h}{\Delta}{P} ~~(h \geq 0)  & \text{adaptable process}\\
	&\sepr&  \scomponent{l}{P}   & \text{located process}\\
	&\sepr&  \adapt{l}{P}{\mathsf{X}}  %\sepr \migrate{l}{m}  \sepr  \destroy{l} 
	& \text{update process}\\
	    & \sepr &   \mathsf{X}& \text{process variable} \\
  	& \sepr &  \ifte{e}{P}{Q} & \text{conditional}\\
  	& \sepr &   P \para  P & \text{parallel composition}\\	 
		&\sepr&   \close{k}.P & \text{close session}	\\
			&\sepr&   \restr{k}{P}  & \text{channel hiding}	\\
			&\sepr&   \mathbf{0}  & \text{inaction} \\
%p	&::= &  + \sepr - &\text{channel polarities} \\
e	&::= &  c &\text{constants} \\
    & \sepr &   e_1 + e_2 \sepr e_1 - e_2  \sepr \mathtt{not}(e) \sepr  \ldots & \text{expressions}
\end{array} 
$$
\caption{Process syntax.} \label{tab:syntax}
\end{table}


We now comment on constructs in Table~\ref{tab:syntax}; in most cases, 
intuitions and conventions are as expected~\cite{DBLP:conf/esop/HondaVK98}.
Prefixes $\nopena{a}{x}$  and $\nopenr{a}{y}$ use name $a$ to establish a new session.
%\jp{We should hint why this is crucial to our approach.}
Once a session is established, structured behavior on channels is possible.
We sometimes refer to $\nopena{a}{x}.P$ as a \emph{service} 
%(for it may accept at most one session request on name $a$)
and to $\repopen{a}{x}.P $ as a \emph{persistent service}. %  (for it may accept zero or more requests on $a$).
In the same vein, we sometimes refer to $\nopenr{a}{x}.Q$ as a \emph{service request}.
Prefix $\close{k}$ is used to explicitly terminate session $k$. 
Having this prefix is crucial to our approach, for it allows us to keep track of the open sessions at any given time.
 The exchange of expressions is as usual; channel passing  
(delegation) is also supported.
Thus, our language supports %the usual dynamic reconfiguration 
transparent distribution of processing 
via channel passing
as well as the more expressive runtime adaptation via \emph{located} and \emph{update processes}, as we discuss below.
%For the sake of simplicity,
With the aim of highlighting the novel aspect of runtime adaptation, 
in this section
we consider infinite behavior in the form of replicated services; %, rather than as recursive definitions;
in \S\,\ref{sec:recsub}
%we do not foresee difficulties in extending our static analyses to a 
we show how to include recursion in the language.\done\todo[A6-A7.]{Here we should point to the new "extensions" section, explicitly mentioning co-inductive definitions.}
Also, we consider a restriction operator over channels only---restriction over names is not 
supported.
%included because we want full transparency.}
%\todo{dire anche qualcosa sul fatto che non c'e' restriction per i session name o per i locality name}


%\newpage
%\todo{nel type system abbiamo associato ad ogni locality l un interfaccia (un tipo) preciso, forse si puo' gia' dire qualcosa qui}

As hinted at in the Introduction, a \emph{located process} $\scomponent{l}{P}$ denotes a
process $P$  deployed at location~$l$.
Inside $l$, process $P$ can evolve on its own and interact with external processes.
In $\scomponent{l}{P}$, we use $l$ as a reference for a potential update action, which 
occurs by interaction with an \emph{update process} $\adapt{l}{Q }{\mathsf{X}}$---a built-in adaptation mechanism.
In $\adapt{l}{Q}{\mathsf{X}}$, 
we use $Q$ to denote a process  with zero or more occurrences of process variable $\mathsf{X}$.
%Intuitively,
As formalized by the operational semantics in~\S\,\ref{ss:opsem},
an \emph{update action} at $l$ corresponds to 
 the interaction of $\scomponent{l}{P}$ and $\adapt{l}{Q}{\mathsf{X}}$ which leads to process 
$Q\subst{P}{\mathsf{X}}$---the process $Q$ in which free occurrences of $\mathsf{X}$ are substituted with $P$.  
In the semantics, we shall consider \emph{annotated} located processes 
$\component{l}{h}{\Delta}{P}$, where $h$ %is a natural which 
stands for the number of active sessions in $P$.
This runtime annotation is used by the type discipline in \S\,\ref{s:types} to ensure that 
update actions do not disrupt the active session behavior deployed at a given location---this is the \emph{consistency} guarantee, formally addressed in \S\,\ref{ss:consist}.\done\todo[B4.]{In this paragraph (but also in the semantics) I have reversed the role of $P$ and $Q$, please check this is consistent.} %, we shall refer to this guarantee as \emph{consistency}.
%Furthermore, for each location $l$, the typing discipline assigns and maintains 
%a \emph{(service) interface} which succinctly describes the  services deployed at $l$.
%The intention is that any update actions on $l$ should at least maintain the service offer as described by its interface.

%$\component{l}{h}{\Delta}{Q}$. 
%$h$ stands for the number of active sessions in $Q$: 
%our operational semantics uses this information to ensure that locations enclosing active 
%sessions are not interrupted by update actions (consistency). 
%\jp{A better approach is to introduce syntax of located processes \emph{without} annotations, saying that $h$ is generated at runtime,
%and that our semantics is instrumented to use $h$.}


%\jp{The following is a bit different now:} In fact, as explained  below, 
%if the \emph{interfaces} of $Q$ and $P$ are 
%\emph{compatible} then 
%processes $\component{l}{h}{\INT_1}{Q}$ and $\adapt{l}{P}{X}$
%may interact so as to \emph{evolve} into $Q\subst{P}{\mathsf{X}}$.  
% Thus, 
% intuitively,
% process $\updated{l}{X}{\INT_1}{\INT_2}{Q}$ 
% behaves as a function which 
% expects a process with interface compatible with $\INT_1$ and 
% returns an adapted process with interface $\INT_2$.

Binding is as follows: 
%the channel 
variable $x$ is bound in processes 
$\nopenr{a}{x}.P$, ~$\repopen{a}{x}.P$, and $\nopena{a}{x}.P$; similarly, 
$\widetilde{x}$ is bound in $\inC{k}{\widetilde{x}}.P$ (variables $x_1, \ldots, x_n$ are all distinct). 
Also, process variable $\mathsf{X}$ is bound in the update process $\adapt{l}{P}{\mathsf{X}}$.
Based on these intuitions, given a process $P$, its sets of free/bound channels, variables, and process variables---noted 
$\mathsf{fc}(P)$, $\mathsf{fv}(P)$, $\mathsf{fpv}(P)$, $\mathsf{bc}(P)$, $\mathsf{bv}(P)$, and $\mathsf{bpv}(P)$, respectively---are defined as expected. 
%We define  $\mathsf{fu}(P) \triangleq \mathsf{fn}(P) \cup \mathsf{fc}(P)$.
%The treatment of recursion variables is also as customary. 
%As for process variables, we assume update processes bind process variables in it. 
%\jp{Free process variables??}
In all cases, we rely on expected notions of $\alpha$-conversion (noted $\equiv_\alpha$) and (capture-avoiding, simultaneous) substitution, noted
$\sub{\widetilde{c}}{\widetilde{x}}$ (for data), $\sub{\kappa^p}{{x}}$ (for channels), and $\sub{P}{\mathsf{X}}$ (for processes).
We work only with closed processes, and often omit the trailing $\nil$.

\subsection{Semantics}\label{ss:opsem}
%\todo{Spiegare bene quando compaiono i Kappa, i kappa compaiono a runtime}

The semantics of our process language is given by 
a \emph{reduction semantics},
denoted $P \pired P'$, the smallest relation on processes generated by the rules in Table~\ref{tab:semantics}.
As customary, it relies on  
an evaluation relation on expressions (noted $e \downarrow c$) and on
a structural congruence relation,  denoted $\equiv$, which we define next.

\begin{definition}[Structural Congruence]\label{d:strcong}
Structural congruence is  
the smallest congruence relation on processes that is generated by the following laws:%\footnote{Cinzia, notice that I have slightly changed the axioms, using $k$ instead of $\kappa$}
$$
\begin{array}{cc}
P \!\para \! Q \!\equiv\! Q \!\para \! P  &
(P \!\para \! Q) \!\para \! R \!\equiv\! P \!\para \! (Q \!\para \! R) \\
P \!\para \! \nil \!\equiv\! P  & 
P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q \\
\restr{\kappa}{\nil} \!\equiv\! \nil & \restr{\kappa}{\restr{\kappa'}{P}} \!\equiv\! \restr{\kappa'}{\restr{\kappa}{P}} \\
\restr{\kappa}{P} \!\para \! Q \!\equiv\! \restr{\kappa}{(P \!\para \! Q)} ~~\text{(if $\kappa \not\in \mathsf{fc}(Q)$)} &
\restr{\kappa}{\component{l}{h}{\Delta}{P}} \!\equiv\! \component{l}{h}{\Delta}{\restr{\kappa}{P}} 
\end{array}
$$
\end{definition}

\begin{table}[t]
{
$$
\begin{array}{ll}
 \rulename{r:Par} & \text{if } P \pired P' ~~\text{then} ~~ P \para Q \pired P' \para Q  \vspace{2mm}
\\
 \rulename{r:Res} &
\text{if } P \pired P' ~~\text{then} ~~ \restr{\cha}{P} \pired \restr{\cha}{P'} %\vspace{2mm} \\
\vspace{2.0mm} \\
 \rulename{r:Str} &
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{2mm}
\\
 \rulename{r:Open} & 
E\big\{C\{\nopena{a}{x}.P\} \para  D\{\nopenr{a}{y}.Q\}\big\} \pired  \\
& 
\hfill E^{++}_{} \big\{\restr{\cha}{\big({C^{+}_{}\{P\sub{\cha^+}{x}\}  \para  D^{+}_{}\{Q\sub{\cha^-}{y}\} }\big)\big\} } \vspace{2.0mm} \\
\rulename{r:ROpen} & 
E\big\{C\{\repopen{a}{x}.P\}  \para  D\{\nopenr{a}{y}.Q\} \big\}  \pired  \\
& 
\hfill E^{++}_{}\big\{\restr{\cha}{\big({C^{+}_{}\{P\sub{\cha^+}{x}  \para \repopen{a}{x}.P \}  \para  D^{+}_{}\{Q\sub{\cha^-}{y}\} }\big)}\big\}  
 \vspace{2.0mm}\\
\rulename{r:Upd} & 
E\big\{C\{\component{l}{0}{}{P}\} \para  D\{\adapt{l}{Q}{X}\}\big\} 
\pired   %\\
%& \hfill 
E_{}\big\{C\{Q\sub{P}{\mathsf{X}}\}  \para  D\{\nil\}\big\} \vspace{2mm} \\
% \srulename{r:Move} & 
% E\big\{C\{\component{l}{h}{}{Q}\} \para  D\{\migrate{l}{m}\}\big\}~~ \pired   
% E_{}\big\{C\{\component{m}{h}{}{Q}\}  \para  D\{\nil\}\big\} \vspace{ 1.5mm} \\
% \srulename{r:Kill} & 
% E\big\{C\{\component{l}{0}{}{Q}\} \para  D\{\destroy{l}\}\big\}~~ 
% \pired   
% E_{}\big\{C\{\nil\}  \para  D\{\nil\}\big\} \vspace{ 1.5mm} \\
\rulename{r:I/O} &
E\big\{C\{\outC{\cha^{\,p}}{\widetilde{e}}.P\} \para  D\{\inC{\cha^{\,\overline{p}}}{\widetilde{x}}.Q\}\big\} 
\pired %\\
%& \hfill 
E\big\{C\{P\} \para  D\{Q\sub{\widetilde{c}\,}{\widetilde{x}}\}\big\} \quad (\widetilde{e} \downarrow \widetilde{c}) \vspace{2mm}
\\
\rulename{r:Pass} &
E\big\{C\{\throw{\cha^{\,p}}{\cha'^{\,q}}.P\} \para  D\{\catch{\cha^{\,\overline{p}}}{x}.Q\}\big\}\pired \hfill E\big\{C^{-}\{P\} \para  D^{+}\{Q\sub{\cha'^{\,q}}{x}\}\big\} %\\
%& \hfill E\big\{C^{-}\{P\} \para  D^{+}\{Q\sub{\cha'^{\,q}}{x}\}\big\} 
\vspace{2mm}
\\
\rulename{r:Sel} &
E\big\{C\{\branch{\cha^{\,p}}{n_1{:}P_1 \alte \cdots \alte n_m{:}P_m}\} \para  D\{\select{\cha^{\,\overline{p}}}{n_j};Q\}\big\} 
\pired \\
& 
\hfill E\big\{C\{P_j\}\para  D\{Q\}\big\}  \quad (1 \leq j \leq m)  \vspace{2mm}
\\
\rulename{r:Close} &
E\big\{C\{\close{\cha^{\,p}}.P\} \para  D\{\close{\cha^{\,\overline{p}}}.Q\}\big\} \pired %\\
%& \hfill 
E^{--}\big\{C^{-}\{P\} \para  D^{-}\{Q\}\big\} \vspace{ 2mm}
\\
\rulename{r:IfTr} &
C\{\ifte{e}{P}{Q}\} \pired C\{P\}  \quad (e \downarrow \mathtt{true})  \vspace{2mm}
\\
 \rulename{r:IfFa} &
C\{\ifte{e}{P}{Q}\} \pired C\{Q\}  \quad (e \downarrow \mathtt{false}) \vspace{2mm}
\end{array}
$$
}
\caption{Reduction semantics. } \label{tab:semantics}
\end{table}
\noindent In Table~\ref{tab:semantics}\done\todo[B5,B6.]{We need to properly answer this comment which concerns the rules.}, duality for polarities $p$ is as expected: $\overline{+} = -$ and $\overline{-} = +$. 
We write $\pired^{*}$ for the reflexive, transitive closure of $\pired$.
As processes can be arbitrarily nested inside %(transparent) 
locations, 
reduction rules use  \emph{contexts}, i.e., processes with a \emph{hole} $\bullet$.


\begin{definition}[Contexts]\label{d:context}
The set of \emph{contexts} is defined by the following syntax:
$$
C, D, E, \ldots ::=\bullet \sepr \component{l}{h}{\Delta}{C \para  P} %\sepr  \sepr \restr{\kappa}{C}  
$$
\end{definition}

%\jp{Why don't we have channel restriction in the syntax of contexts?}
%This way, g
Given a context $C$ 
%$C\{\bullet\}$ 
and a process $P$, 
we write $C\{P\}$ to denote the process obtained by filling in the occurrences of hole $\bullet$ in $C$ with $P$.
The intention is that $P$ may reduce inside $C$, thus reflecting the transparent containment realized by location nesting.\done\todo[B7.]{Add a sentence that is aligned with the reviewer's confusion and with the specific role that contexts play in our model. Perhaps we could call them "locating context" or something...}

We assume the expected extension of $\equiv$ to contexts; in particular, we tacitly use $\equiv$ to enlarge the scope of restricted channels in contexts as needed. As mentioned above, reduction relies on located processes with annotations $h$, which denote the number of active sessions at every location.
To ensure the coherence of such annotations along reduction, 
 we define operations over contexts
 which allow us to increase/de\-crease the annotation $h$ on every location contained in a context. 
 
 \begin{definition}[Operations on Contexts] \label{d:opcontx}
Given a context $C$ as in Def.~\ref{d:context}, a natural number $j$,
and an operator $* \in \{+,-\}$, %and $ \otimes \in \{\addelta, \midelta \}$, 
we define $C^{*j}$ as follows: 
$$ (\bullet)^{*j}_{}  = \bullet \qquad~~ (\component{l}{h}{\Delta}{C \para P})^{*j}_{} = \component{l}{{h*j}}{\Delta}{C^{*j}_{} \para P} %\quad~~ (C \para  P)^{*j}_{} = C^{*j}_{} \para  P 
$$
\end{definition}

This way, for instance, ${C}^{+1}$ 
denotes the context $C$ in which 
 the runtime annotations for all locations have been incremented by one.
We  write ${C}^{-}$, ${C}^{+}$, ${C}^{--}$, and ${C}^{++}$ to stand for ${C}^{-1}$, ~${C}^{+1}$, ${C}^{-2}$, and ${C}^{+2}$, respectively.


We now comment on reduction rules \rulename{r:Open}, \rulename{r:Upd}, \rulename{r:Pass}, and \rulename{r:Close} in Table~\ref{tab:semantics}; 
other rules are either standard or self-explanatory.

Rule \rulename{r:Open} formalizes session establishment. There are three distinguished contexts: while $C$ contains the %(linear) 
service offer and 
$D$ encloses the service request, context $E$ encloses both $C$ and $D$. %\done\todo[B9.]{We have said in Sect 2.1. that a linear service may execute at most once.}
By matching on name $a$ a session is established; 
following~\cite{DBLP:journals/acta/GayH05,DBLP:journals/entcs/YoshidaV07}, 
this is realized by endowing each partner with a fresh polarized channel (or end-point) $\kappa^p$.
As such, channels $\kappa^+$ and $\kappa^-$ are runtime entities. 
%with a fresh channel $c$; \jp{This is the point where we should explain runtime $\kappa$} at runtime, each process gets one end of the channel.
Because of session initiation, the number of active sessions 
should be increased across all enclosing contexts: relying on the operators given in Def.~\ref{d:opcontx}, we increment by one in contexts $C$ and $D$ and by two in context $E$, for it encloses both endpoints. 
This increment realizes a form of protection against careless update actions; observe that due to the  transparency of locations, any updates may take place independently from the actual nested structure.

The reasons for the increment just described should be clear from rule \rulename{r:Upd}, which formalizes the update/reconfiguration of a location $l$, 
enclosed in contexts $C$ and $E$.  
Notice how the update action can only occur if the number of open (active) sessions in $l$ is 0.
By forcing updates to occur only when any (located) session behavior has completed (cf. rule \rulename{r:Close}), reduction ensures that 
active sessions are not inadvertently disrupted. %update actions which may interrupt session communications.
When enabled, an update action  is  realized by 
  substituting, within location $l$, all free occurrences of $\mathsf{X}$ in $Q$ with $P$ (the current behavior at $l$). Hence,  it is the adaptation routine which ``moves''   to realize reconfiguration. This is a form of \emph{objective update}, as the located process does not 
contain information on future update actions: it reduces autonomously until it is adapted by an update process in its environment. 

Rule \rulename{r:Pass} is the standard rule for delegation; in our setting, endpoint mobility is reflected by appropriate decrements/increments in the contexts enclosing the session sender/receiver. 
Rule~\rulename{r:Close} formalizes the synchronized session closure. In analogy with rule \rulename{r:Open}, session closure 
should decrease the active session annotation in all enclosing contexts.
%\jp{We no longer need to refer to interfaces here, only to the fact that runtime annotation $h$ is used to avoid inconsistent updates}
%Let us write $\intf{P}$ for the \emph{interface} of process $P$ (cf. Sect.~\ref{s:types}). 

\subsection{Examples of Runtime Adaptation}\label{ss:examp}

%\begin{example}
%In order to illustrate the syntax and semantics of our framework, 
We now present 
some patterns of runtime adaptation that can be expressed in our process framework.
Recall that $l_1, l_2, \ldots$ denote identifiers for locations.
We discuss different reductions, resulting from the interaction between a located process and a corresponding adaptable process.
These reductions are \emph{enabled}; for the sake of readability, however, we elide the runtime annotation 
associated to the locations ($h = 0$ in all cases).


%We give here some examples on how adaptable processes can be used:
 \begin{description}
 \item[Relocation.] One of the simplest reconfiguration actions that 
 can be represented in our model is the relocation of an arbitrary behavior %at a location 
 to a completely different
 computation site. 
 The following reduction illustrates how a synchronization on location $l_1$ leads to 
 a relocation from $l_1$ to $l_2$:
% Similarly, one can think of moving the content of a locality $a$ into a fresh locality $b$:
$$\bigcomponent{l_1}{}{}{\,\compo{l_4}{}{Q}\,} \para \adapt{l_1}{\compo{l_2}{}{ \mathsf{X} }}{ \mathsf{X} } \pired \bigcomponent{l_2}{}{}{\,\compo{l_4}{}{Q}\,} \para \nil $$
It is worth observing how a relocation does not alter the behavior at $l_1$.
In particular, relocations are harmless to open sessions in $Q$, if any.
 
\item[Deep Update.] 
Because our locations are transparent, an update action may have influence on located processes not necessarily at top-level
in the nested process structure. 
The reduction below illustrates how the influence of an update process on name $l_3$ can cross locations $l_1$ and $l_2$ in order
to realize an adaptation routine, represented by process $S'$:
%We start with an example that underlines the transparency of adaptable processes, here we are going to substitute the adaptable process located at $c$ with a new adaptable process $S'$ located inside $d$. Notice that $c$ occurs inside $b$ that is on its turn inside $a$. Thus:
$$\bigcomponent{l_1}{}{}{Q \para \bigcomponent{l_2}{}{}{R \para \compo{l_3}{}{S_{1}} }\,} \para 
\adapt{l_3}{\compo{l_4}{}{S'}}{ \mathsf{X} } 
\pired 
\bigcomponent{l_1}{}{}{Q \para \compo{l_2}{}{R \para \compo{l_4}{}{S_{2}}\, }\, } \para \nil $$
where $S_2 = S'\sub{S_1}{\mathsf{X}}$.
That is, by virtue of the update action on $l_3$, its current behavior  (denoted $S_1$) is suspended 
and possibly used in the new behavior $S'$, which is now located at~$l_4$.

 \item[Upgrade.] Interestingly, update actions do not need to preserve the current behavior at a given location. 
 In fact, if the adaptation routine embodied by the updated process does not contain a process variable, 
 then the current behavior at the location will be discarded.
 This feature is illustrated by the following reduction, in which we assume that $\mathsf{X} \notin \mathsf{fv}(Q)$:
 % Next, we show how to destroy locality $a$ and its content. In this case we require $\mathsf{X} \notin \mathsf{fv}(Q)$, this way $Q$ is a closed process and $Q\sub{P}{\mathsf{X}}= Q$ thus obtaining:
$$ \compo{l_1}{}{P} \para \adapt{l_1}{Q}{\mathsf{X}} \pired Q \para \nil $$
Observe that the location on which the update action takes place does not need to be preserved either:
had we wanted to only replace the behavior at $l_1$, then it would have sufficed\done\todo[B29.]{Fixed, pls check.} to enclose 
the runtime adaptation code $Q$ within a located process named $l_1$, i.e.,
%recreate the locality $a$ in the update construct:  
$\adapt{l_1}{\compo{l_1}{}{Q}}{\mathsf{X}}$. 


\item[Conditional Backup.]   The current behavior of a location may be used more than once by an
adaptation routine.
Consider process $B_e$ below:
$$
B_e = \compo{l_1}{}{Q} \para \bigcomponent{l_5}{}{}{\,
\ifte{e}{\adapt{l_1}{\compo{l_2}{}{\mathsf{X}}}{\mathsf{X}}}{\adapt{l_1}{\compo{l_1}{}{\mathsf{X}}{} \para \compo{l_3}{}{\mathsf{X}}}{\mathsf{X}}}\,}
$$
Depending on the boolean expression $e$ reduces to, 
$B_e$ may either (i) simply relocate the behavior at $l_1$, 
or (ii) define a ``backup copy''  of $Q$ at  $l_3$: %. More precisely:
\begin{eqnarray*}
B_e & \pired^* & \compo{l_2}{}{Q} \para \compo{l_5}{}{\nil} \quad \qquad \qquad\text{if $e \downarrow \mathtt{true}$} \\
B_e & \pired^* & \compo{l_1}{}{Q} \para \compo{l_3}{}{Q} \para \compo{l_5}{}{\nil} \qquad\text{if $e \downarrow \mathtt{false}$}
\end{eqnarray*}
\end{description}

\noindent
The previous examples are useful to illustrate the expressiveness of adaptable processes for representing 
rich  adaptation mechanisms. As our process model includes both communication and update actions,
we require mechanisms for harmonizing %both kinds of actions, 
them, \done\todo[B30.]{Fixed, pls check.}
avoiding undesirable disruptions of communication behavior by updates.
In the next section, we define a static analysis technique that enables update actions when 
the given location does not enclose open sessions.


